AN AXIOMATIZATION OF KNOWLEDGE AND THE EXAMPLE OF THE WISE MAN PUZZLE


	This memo reports results  of a part of long  continuing work
on  the axiomatization  of knowledge for  the purposes  of artificial
intelligence.  Unfortunately, little of that work has  been published
even informally, and this is a piece out of the middle, so to speak.

	It  is  derived from  the  author's  modal axiomatization  of
knowledge, but  is more directly based on a Kripke type semantics for
that modal  system given  by M.  Sato of  Kyoto Univerity.   It  owes
considerable to  discussions with Professors Takasu  and Igarashi and
Messrs. Hayashi and Sato of Kyoto University.

	That axiomatization  is  distinguished  from  others  in  the
literature by the  presence of an  individual called FOOL,  such that
anything FOOL knows, he knows that every one knows.

	We work  in the first order logic  system associated with the
FOL proof-checker of Weyhrauch.

	There  are  three  sorts   of  individuals  called   persons,
propositions, and worlds.  Each variable  is confined to one of these
sorts,  and  the  sort  mechanism of  FOL  restricts  the  meaning of
quantification of a variable to the appropriate sort.

	The first  predicate is T(proposition,world)  and means  that
the  proposition  is  true  in  the  world.    There  is  a  function
K(person,proposition) which is  a proposition  asserting that  person
knows the proposition serving as argument.   The propositions of this
system are  individuals with respect to the  first order logic rather
than truth values or wffs.  Therefore, we have to expicitly introduce
proposition-valued   functions  AND,   OR,  IMP,   EQUIV,  and   NOT,
corresponding to the logical connectives ∧, ∨, ⊃, ≡, and ¬.  Finally,
KW(s,p) is introduced as an abbreviation for K(s,p) ∨ K(s,NOT(p)) and
is read "s knows whether p".

	Here is  the axiom system in FOL  notation.  The declarations
establish the types of the variables  and constants.  The axioms  are
essentially all  definitions except for  REFLEX which asserts  that a
world is accessible from itself for any person.

DECLARE INDCONST FOOL ε PERSON;

DECLARE INDVAR S S1 S2 S3 S4 ε PERSON;
DECLARE INDVAR W W1 W2 W3 ε WORLD;
DECLARE INDVAR P P1 P2 P3 P4 Q Q1 Q2 Q3 Q4 R R1 R2 R3 R4 ε PROPOSITION;

DECLARE OPCONST K(PERSON,PROPOSITION) = PROPOSITION;
DECLARE OPCONST KW(PERSON,PROPOSITION) = PROPOSITION;
DECLARE OPCONST AND(PROPOSITION,PROPOSITION) = PROPOSITION;
DECLARE OPCONST OR(PROPOSITION,PROPOSITION) = PROPOSITION;
DECLARE OPCONST IMP(PROPOSITION,PROPOSITION) = PROPOSITION;
DECLARE OPCONST EQUIV(PROPOSITION,PROPOSITION) = PROPOSITION;
DECLARE OPCONST NOT(PROPOSITION) = PROPOSITION;

DECLARE PREDCONST T(PROPOSITION,WORLD);
DECLARE PREDCONST A(PERSON,WORLD,WORLD);

AXIOM REFLEX: ∀ S W.(A(S,W,W));;

AXIOM KNOW: ∀ S P W.(T(K(S,P),W) ≡ ∀W1.(A(S,W,W1) ⊃ T(P,W1)));;

AXIOM KW: ∀ S P W.(T(KW(S,P),W) ≡ T(K(S,P),W) ∨ T(K(S,NOT(P)),W));;

AXIOM FOOL: ∀ S P W.(T(K(FOOL,P),W) ⊃ T(K(FOOL,K(S,P)),W));;

AXIOM AND: ∀ W P Q.(T(AND(P,Q),W) ≡ T(P,W) ∧ T(Q,W));;
AXIOM OR: ∀ W P Q.(T(OR(P,Q),W) ≡ T(P,W) ∨ T(Q,W));;
AXIOM IMP: ∀ W P Q.(T(IMP(P,Q),W) ≡ T(P,W) ⊃ T(Q,W));;
AXIOM EQUIV: ∀ W P Q.(T(EQUIV(P,Q),W) ≡ (T(P,W) ≡ T(Q,W)));;
AXIOM NOT: ∀ W P.(T(NOT(P),W) ≡ ¬T(P,W));;

	As an example of the use of these axioms, we do the following
puzzle of the three wise men.

	"A  certain king paints white  spots on the  foreheads of his
three wisemen who can see each  other and are told that at least  one
spot is  white and the  others black.   He asks  if any can  tell the
color of  his spot and after a while the wisest affirms that his spot
is white.  The puzzle is to tell how he knows."

	The solution is  to say that  the wisest reasons as  follows:
"If my spot  were black, the smarter of the  remaining two would have
seen it and reasoned that if his  spot were black, the slowest of  us
would have seen two black spots and reasoned that his must be white."

	In this form, the puzzle requires the  wisest to reason about
how fast his colleagues think.  We can get rid of this at the cost of
unfairness by  having the  king as  each wise  man in  turn with  the
answer being audible to the others.   Another solution would have the
king  not accept  volunteered answers  but repeat the  question three
times,  getting the  correct  answer  from  all three  on  the  third
repetition.

	Here are the axioms describing the puzzle:

DECLARE INDCONST WISE1 WISE2 WISE3 ε PERSON;
DECLARE INDCONST RW ε WORLD;
DECLARE INDCONST WHITE1 WHITE2 WHITE3 εPROPOSITION;

AXIOM WISEMAN:
	T(WHITE1,RW)∧T(WHITE2,RW)∧T(WHITE3,RW),
	T(K(FOOL,KW(WISE1,WHITE2)),RW),
	T(K(FOOL,KW(WISE1,WHITE3)),RW),
	T(K(FOOL,KW(WISE2,WHITE1)),RW),
	T(K(FOOL,KW(WISE2,WHITE3)),RW),
	T(K(FOOL,KW(WISE3,WHITE1)),RW),
	T(K(FOOL,KW(WISE3,WHITE2)),RW),
	T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),RW),

	T(K(WISE3,K(WISE2,NOT(K(WISE1,WHITE1)))),RW),
	T(K(WISE3,NOT(K(WISE2,WHITE2))),RW);
;

	Next follows an annotated version of  the FOL proof. Included
in the  proof are the proofs  of four lemmas that  depend only on the
knowledge axioms and not on the specifics of the wise man puzzle.